Left Termination of the query pattern
perm1(g,g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 84 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 27 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇔, 5 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇔, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇔, 0 ms)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔, 0 ms)
        ↳27 YES

(0) Obligation:

Clauses:

perm1(L, M) :- ','(eq_len1(L, M), same_sets(L, M)).
eq_len1([], []).
eq_len1(.(X1, Xs), .(X2, Ys)) :- eq_len1(Xs, Ys).
member(X, .(X, X3)).
member(X, .(X4, T)) :- member(X, T).
same_sets([], X5).
same_sets(.(X, Xs), L) :- ','(member(X, L), same_sets(Xs, L)).

Query: perm1(g,g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

eq_len1A(.(X1, X2), .(X3, X4)) :- eq_len1A(X2, X4).
memberB(X1, .(X2, X3)) :- memberB(X1, X3).
pC(X1, X2, X3, X4) :- memberB(X1, X3).
pC(X1, X2, X3, .(X4, X5)) :- ','(membercD(X1, X2, X3), pC(X4, X2, X3, X5)).
perm1E(.(X1, X2), .(X3, X4)) :- eq_len1A(X2, X4).
perm1E(.(X1, X2), .(X3, X4)) :- ','(eq_len1cA(X2, X4), pC(X1, X3, X4, X2)).

Clauses:

eq_len1cA([], []).
eq_len1cA(.(X1, X2), .(X3, X4)) :- eq_len1cA(X2, X4).
membercB(X1, .(X1, X2)).
membercB(X1, .(X2, X3)) :- membercB(X1, X3).
qcC(X1, X2, X3, []) :- membercD(X1, X2, X3).
qcC(X1, X2, X3, .(X4, X5)) :- ','(membercD(X1, X2, X3), qcC(X4, X2, X3, X5)).
membercD(X1, X1, X2).
membercD(X1, X2, X3) :- membercB(X1, X3).

Afs:

perm1E(x1, x2)  =  perm1E(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
perm1E_in: (b,b)
eq_len1A_in: (b,b)
eq_len1cA_in: (b,b)
pC_in: (b,b,b,b)
memberB_in: (b,b)
membercD_in: (b,b,b)
membercB_in: (b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

PERM1E_IN_GG(.(X1, X2), .(X3, X4)) → U6_GG(X1, X2, X3, X4, eq_len1A_in_gg(X2, X4))
PERM1E_IN_GG(.(X1, X2), .(X3, X4)) → EQ_LEN1A_IN_GG(X2, X4)
EQ_LEN1A_IN_GG(.(X1, X2), .(X3, X4)) → U1_GG(X1, X2, X3, X4, eq_len1A_in_gg(X2, X4))
EQ_LEN1A_IN_GG(.(X1, X2), .(X3, X4)) → EQ_LEN1A_IN_GG(X2, X4)
PERM1E_IN_GG(.(X1, X2), .(X3, X4)) → U7_GG(X1, X2, X3, X4, eq_len1cA_in_gg(X2, X4))
U7_GG(X1, X2, X3, X4, eq_len1cA_out_gg(X2, X4)) → U8_GG(X1, X2, X3, X4, pC_in_gggg(X1, X3, X4, X2))
U7_GG(X1, X2, X3, X4, eq_len1cA_out_gg(X2, X4)) → PC_IN_GGGG(X1, X3, X4, X2)
PC_IN_GGGG(X1, X2, X3, X4) → U3_GGGG(X1, X2, X3, X4, memberB_in_gg(X1, X3))
PC_IN_GGGG(X1, X2, X3, X4) → MEMBERB_IN_GG(X1, X3)
MEMBERB_IN_GG(X1, .(X2, X3)) → U2_GG(X1, X2, X3, memberB_in_gg(X1, X3))
MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)
PC_IN_GGGG(X1, X2, X3, .(X4, X5)) → U4_GGGG(X1, X2, X3, X4, X5, membercD_in_ggg(X1, X2, X3))
U4_GGGG(X1, X2, X3, X4, X5, membercD_out_ggg(X1, X2, X3)) → U5_GGGG(X1, X2, X3, X4, X5, pC_in_gggg(X4, X2, X3, X5))
U4_GGGG(X1, X2, X3, X4, X5, membercD_out_ggg(X1, X2, X3)) → PC_IN_GGGG(X4, X2, X3, X5)

The TRS R consists of the following rules:

eq_len1cA_in_gg([], []) → eq_len1cA_out_gg([], [])
eq_len1cA_in_gg(.(X1, X2), .(X3, X4)) → U10_gg(X1, X2, X3, X4, eq_len1cA_in_gg(X2, X4))
U10_gg(X1, X2, X3, X4, eq_len1cA_out_gg(X2, X4)) → eq_len1cA_out_gg(.(X1, X2), .(X3, X4))
membercD_in_ggg(X1, X1, X2) → membercD_out_ggg(X1, X1, X2)
membercD_in_ggg(X1, X2, X3) → U15_ggg(X1, X2, X3, membercB_in_gg(X1, X3))
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
membercB_in_gg(X1, .(X2, X3)) → U11_gg(X1, X2, X3, membercB_in_gg(X1, X3))
U11_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))
U15_ggg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercD_out_ggg(X1, X2, X3)

Pi is empty.
We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PERM1E_IN_GG(.(X1, X2), .(X3, X4)) → U6_GG(X1, X2, X3, X4, eq_len1A_in_gg(X2, X4))
PERM1E_IN_GG(.(X1, X2), .(X3, X4)) → EQ_LEN1A_IN_GG(X2, X4)
EQ_LEN1A_IN_GG(.(X1, X2), .(X3, X4)) → U1_GG(X1, X2, X3, X4, eq_len1A_in_gg(X2, X4))
EQ_LEN1A_IN_GG(.(X1, X2), .(X3, X4)) → EQ_LEN1A_IN_GG(X2, X4)
PERM1E_IN_GG(.(X1, X2), .(X3, X4)) → U7_GG(X1, X2, X3, X4, eq_len1cA_in_gg(X2, X4))
U7_GG(X1, X2, X3, X4, eq_len1cA_out_gg(X2, X4)) → U8_GG(X1, X2, X3, X4, pC_in_gggg(X1, X3, X4, X2))
U7_GG(X1, X2, X3, X4, eq_len1cA_out_gg(X2, X4)) → PC_IN_GGGG(X1, X3, X4, X2)
PC_IN_GGGG(X1, X2, X3, X4) → U3_GGGG(X1, X2, X3, X4, memberB_in_gg(X1, X3))
PC_IN_GGGG(X1, X2, X3, X4) → MEMBERB_IN_GG(X1, X3)
MEMBERB_IN_GG(X1, .(X2, X3)) → U2_GG(X1, X2, X3, memberB_in_gg(X1, X3))
MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)
PC_IN_GGGG(X1, X2, X3, .(X4, X5)) → U4_GGGG(X1, X2, X3, X4, X5, membercD_in_ggg(X1, X2, X3))
U4_GGGG(X1, X2, X3, X4, X5, membercD_out_ggg(X1, X2, X3)) → U5_GGGG(X1, X2, X3, X4, X5, pC_in_gggg(X4, X2, X3, X5))
U4_GGGG(X1, X2, X3, X4, X5, membercD_out_ggg(X1, X2, X3)) → PC_IN_GGGG(X4, X2, X3, X5)

The TRS R consists of the following rules:

eq_len1cA_in_gg([], []) → eq_len1cA_out_gg([], [])
eq_len1cA_in_gg(.(X1, X2), .(X3, X4)) → U10_gg(X1, X2, X3, X4, eq_len1cA_in_gg(X2, X4))
U10_gg(X1, X2, X3, X4, eq_len1cA_out_gg(X2, X4)) → eq_len1cA_out_gg(.(X1, X2), .(X3, X4))
membercD_in_ggg(X1, X1, X2) → membercD_out_ggg(X1, X1, X2)
membercD_in_ggg(X1, X2, X3) → U15_ggg(X1, X2, X3, membercB_in_gg(X1, X3))
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
membercB_in_gg(X1, .(X2, X3)) → U11_gg(X1, X2, X3, membercB_in_gg(X1, X3))
U11_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))
U15_ggg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercD_out_ggg(X1, X2, X3)

Pi is empty.
We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 10 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)

The TRS R consists of the following rules:

eq_len1cA_in_gg([], []) → eq_len1cA_out_gg([], [])
eq_len1cA_in_gg(.(X1, X2), .(X3, X4)) → U10_gg(X1, X2, X3, X4, eq_len1cA_in_gg(X2, X4))
U10_gg(X1, X2, X3, X4, eq_len1cA_out_gg(X2, X4)) → eq_len1cA_out_gg(.(X1, X2), .(X3, X4))
membercD_in_ggg(X1, X1, X2) → membercD_out_ggg(X1, X1, X2)
membercD_in_ggg(X1, X2, X3) → U15_ggg(X1, X2, X3, membercB_in_gg(X1, X3))
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
membercB_in_gg(X1, .(X2, X3)) → U11_gg(X1, X2, X3, membercB_in_gg(X1, X3))
U11_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))
U15_ggg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercD_out_ggg(X1, X2, X3)

Pi is empty.
We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)
    The graph contains the following edges 1 >= 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PC_IN_GGGG(X1, X2, X3, .(X4, X5)) → U4_GGGG(X1, X2, X3, X4, X5, membercD_in_ggg(X1, X2, X3))
U4_GGGG(X1, X2, X3, X4, X5, membercD_out_ggg(X1, X2, X3)) → PC_IN_GGGG(X4, X2, X3, X5)

The TRS R consists of the following rules:

eq_len1cA_in_gg([], []) → eq_len1cA_out_gg([], [])
eq_len1cA_in_gg(.(X1, X2), .(X3, X4)) → U10_gg(X1, X2, X3, X4, eq_len1cA_in_gg(X2, X4))
U10_gg(X1, X2, X3, X4, eq_len1cA_out_gg(X2, X4)) → eq_len1cA_out_gg(.(X1, X2), .(X3, X4))
membercD_in_ggg(X1, X1, X2) → membercD_out_ggg(X1, X1, X2)
membercD_in_ggg(X1, X2, X3) → U15_ggg(X1, X2, X3, membercB_in_gg(X1, X3))
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
membercB_in_gg(X1, .(X2, X3)) → U11_gg(X1, X2, X3, membercB_in_gg(X1, X3))
U11_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))
U15_ggg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercD_out_ggg(X1, X2, X3)

Pi is empty.
We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PC_IN_GGGG(X1, X2, X3, .(X4, X5)) → U4_GGGG(X1, X2, X3, X4, X5, membercD_in_ggg(X1, X2, X3))
U4_GGGG(X1, X2, X3, X4, X5, membercD_out_ggg(X1, X2, X3)) → PC_IN_GGGG(X4, X2, X3, X5)

The TRS R consists of the following rules:

membercD_in_ggg(X1, X1, X2) → membercD_out_ggg(X1, X1, X2)
membercD_in_ggg(X1, X2, X3) → U15_ggg(X1, X2, X3, membercB_in_gg(X1, X3))
U15_ggg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercD_out_ggg(X1, X2, X3)
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
membercB_in_gg(X1, .(X2, X3)) → U11_gg(X1, X2, X3, membercB_in_gg(X1, X3))
U11_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PC_IN_GGGG(X1, X2, X3, .(X4, X5)) → U4_GGGG(X1, X2, X3, X4, X5, membercD_in_ggg(X1, X2, X3))
U4_GGGG(X1, X2, X3, X4, X5, membercD_out_ggg(X1, X2, X3)) → PC_IN_GGGG(X4, X2, X3, X5)

The TRS R consists of the following rules:

membercD_in_ggg(X1, X1, X2) → membercD_out_ggg(X1, X1, X2)
membercD_in_ggg(X1, X2, X3) → U15_ggg(X1, X2, X3, membercB_in_gg(X1, X3))
U15_ggg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercD_out_ggg(X1, X2, X3)
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
membercB_in_gg(X1, .(X2, X3)) → U11_gg(X1, X2, X3, membercB_in_gg(X1, X3))
U11_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))

The set Q consists of the following terms:

membercD_in_ggg(x0, x1, x2)
U15_ggg(x0, x1, x2, x3)
membercB_in_gg(x0, x1)
U11_gg(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U4_GGGG(X1, X2, X3, X4, X5, membercD_out_ggg(X1, X2, X3)) → PC_IN_GGGG(X4, X2, X3, X5)
    The graph contains the following edges 4 >= 1, 2 >= 2, 6 > 2, 3 >= 3, 6 > 3, 5 >= 4

  • PC_IN_GGGG(X1, X2, X3, .(X4, X5)) → U4_GGGG(X1, X2, X3, X4, X5, membercD_in_ggg(X1, X2, X3))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 4 > 5

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

EQ_LEN1A_IN_GG(.(X1, X2), .(X3, X4)) → EQ_LEN1A_IN_GG(X2, X4)

The TRS R consists of the following rules:

eq_len1cA_in_gg([], []) → eq_len1cA_out_gg([], [])
eq_len1cA_in_gg(.(X1, X2), .(X3, X4)) → U10_gg(X1, X2, X3, X4, eq_len1cA_in_gg(X2, X4))
U10_gg(X1, X2, X3, X4, eq_len1cA_out_gg(X2, X4)) → eq_len1cA_out_gg(.(X1, X2), .(X3, X4))
membercD_in_ggg(X1, X1, X2) → membercD_out_ggg(X1, X1, X2)
membercD_in_ggg(X1, X2, X3) → U15_ggg(X1, X2, X3, membercB_in_gg(X1, X3))
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
membercB_in_gg(X1, .(X2, X3)) → U11_gg(X1, X2, X3, membercB_in_gg(X1, X3))
U11_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))
U15_ggg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercD_out_ggg(X1, X2, X3)

Pi is empty.
We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

EQ_LEN1A_IN_GG(.(X1, X2), .(X3, X4)) → EQ_LEN1A_IN_GG(X2, X4)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

EQ_LEN1A_IN_GG(.(X1, X2), .(X3, X4)) → EQ_LEN1A_IN_GG(X2, X4)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • EQ_LEN1A_IN_GG(.(X1, X2), .(X3, X4)) → EQ_LEN1A_IN_GG(X2, X4)
    The graph contains the following edges 1 > 1, 2 > 2

(27) YES